% RA: Relación 02
% OTTER: puzle3.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% Un puzle está compuesto por las siguientes cuatro fichas:
%
%         +----+        +----+        +----+        +----+
%         |\BB/|        |\RR/|        |\AA/|        |\BB/|
%         |R\/V|        |V\/R|        |A\/V|        |R\/A|
%         |R/\V|        |V/\R|        |A/\V|        |R/\A|
%         |/VV\|        |/BB\|        |/BB\|        |/RR\|
%         +----+        +----+        +----+        +----+
%
% Donde B, R, V y A representan los colores Blanco, Rojo, Verde y Azul,
% respectivamente. 
%
% Utilizar OTTER para encontrar todas las maneras posibles de colocar estas
% cuatro fichas en un cuadrado de dimensión 2x2, sin repetir, de forma lo
% colores de los lados adyacentes coincidan. En este caso las fichas se pueden
% girar.

%==============================================================================
% Formalización
%==============================================================================

% Configuración del sistema

% set(auto2).

set(hyper_res).
% set(para_from).
% set(para_into).
assign(max_proofs,-1).

% Este ejercicio es una variante del ejercicio anterior en el que cada ficha
% tiene 4 orientaciones posibles y el resultado tiene que formar un cuadrado de
% tamaño 2x2 en número de fichas.

formula_list(sos).
 all x (x = x).
 all x y (x = y -> y = x).
 all x y z (x = y & y = z -> x = z).

 1 != 2.
 1 != 3.
 1 != 4.
 2 != 3.
 2 != 4.
 3 != 4.

 all x1 x2 x3 x4 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  ((ficha(x1,y1,y2,y3,y4) & ficha(x2,y3,y5,y6,y7) &
    ficha(x3,y8,y4,y9,y10) & ficha(x4,y9,y7,y11,y12) &
    $NE(x1,x2) & $NE(x1,x3) & $NE(x1,x4) &
    $NE(x2,x3) & $NE(x2,x4) & $NE(x3,x4)) ->
   posicion(x1,[y1,y2,y3,y4],x2,[y3,y5,y6,y7],
            x3,[y8,y4,y9,y10],x4,[y9,y7,y11,y12])).

 ficha(1,rojo,blanco,verde,verde).
 ficha(2,verde,rojo,rojo,blanco).
 ficha(3,azul,azul,verde,blanco).
 ficha(4,rojo,blanco,azul,rojo).

% all x y1 y2 y3 y4 (ficha(x,y1,y2,y3,y4) ->
%           ficha(x,y2,y3,y4,y1) & ficha(x,y3,y4,y1,y2) & ficha(x,y4,y1,y2,y3)).

% Es suficiente con describir el giro de 90 grados.
all x y1 y2 y3 y4 (ficha(x,y1,y2,y3,y4) -> ficha(x,y2,y3,y4,y1)).

end_of_list.

formula_list(passive).
 all x1 x2 x3 x4 o1 o2 o3 o4
   (posicion(x1,o1,x2,o2,x3,o3,x4,o4) -> $ANS(x1,o1,x2,o2,x3,o3,x4,o4)).
end_of_list.

%==============================================================================
